T:Type, P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B)) 

latex

Definitions	if b t else f fi, as @ bs, Unit, P  Q, P & Q, P  Q, , Prop, b, A, b, Top, x:A. B(x), t  T
Lemmas	assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf